COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	COMMENT% This is a collection of theorems in set theory - hopefully
C00004 ENDMK
C⊗;
COMMENT% This is a collection of theorems in set theory - hopefully
of general utility rather than ad hoc for specific problems.  It is
intended to be used in conjunction with HEAVY.AX[W76,JMC].  In
principle, all these theorems could be proved from the axioms
in HEAVY.AX, but this hasn't been done.%

DECLARE INDCONST CARDS Card ε CLASS;

AXIOM Card:	Card = {a|∃b.a = <b,card(b)>},
		CARDS = {a|CARD(a)},
		∀a.(card(a) = apply(Card,a)),

		card(λ) = 0,
		∀x.(card({x}) = 1),
		∀a b.(card(a∪b)+card(a∩b) = card(a)+card(b)),
		∀a b.(card(CROSS(a,b)) = card(a)*card(b));;


COMMENT% The operand of SUM is a function whose RNG consists of cardinal
numbers, and its value is the sum of these numbers.%

AXIOM SUM:	SUM(λ) = 0,
		∀a b.(CARD(b) ⊃ SUM({<a,b>}) = b),
		∀c a1 a2.(RNG(c) ⊂ CARDS ⊃
	SUM(c|(a1∪a2))+SUM(c|(a1∩a2)) = SUM(c|a1)+SUM(c|a2)),

DEFINE DISJOINT:∀M.(DISJOINT(M) ≡ ∀a1 a2.(a1εM ∧ a2εM ⊃ a1=a2 ∨ a1∩a2 =λ));;

AXIOM CARDP:	∀a.(DISJOINT(a) ⊃ card(UNION(a)) = SUM(Card|a);;
	


AXIOM SET:	∀a b.(CROSS(a,b) = UNION({d|∃c.(cεa ∧ d = CROSS({c},b))})),

		∀a b.(UNION(a)∩b = UNION({d|∃c.(cεa ∧ d = c∩b)}),